Inference at * 1 1 
Iof proof for Lemma sub-equality:

.....assertion..... NILNIL

1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
  P(i) 

latex

 by (HypSubst (-2) 0) 
CollapseTHEN (Auto) 

latex

C.

Definitions

t  T, f(a)